Inference at * 1 
Iof proof for Lemma inconsistent-bool-eq3:



1. b : 
2. b
  (tt = ff)  False 

latex

 by (RWO "inconsistent-bool-eq" 0) 
CollapseTHEN (Auto) 

latex

C.

Definitions	s = t, , x:A. B(x), x:A  B(x), x:AB(x), P  Q, P & Q, P  Q, P  Q, False
Lemmas	iff functionality wrt iff, inconsistent-bool-eq, false wf